let h [p] (f, x) where (p (x) and (p (x) => pre (f) (x)))
returns z where (p (x))
=
 f (x)

let g (x) where (x >= 0) returns y where (x = y) 
= x

predicate positive (x) = x > 0

let x = h [positive] (g, 1)
  
